Nuprl Lemma : map-concat
0,22
postcript
pdf
f
:(Top
Top),
L
:(Top List) List. map(
f
;concat(
L
)) ~ concat(map(
l
.map(
f
;
l
);
L
))
latex
Definitions
map(
f
;
as
)
,
x
:
A
.
B
(
x
)
,
t
T
,
Top
Lemmas
top
wf
,
map
append
sq
,
map
wf
,
concat-cons
origin
f:(Top
Top), L:(Top List) List. map(f;concat(L)) ~ concat(map(
l.map(f;l);L)) f:(TopTop), L:(Top List) List. map(f;concat(L)) ~ concat(map(l.map(f;l);L)) x:A. B(x)
T